import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
_s, _t, _ket_u, _U, _phase, _s_in_nat_pos, _u_ket_register,
_normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
QPE1_def, _psi_t_def, _psi_t_ket_is_normalized_vec)
theory = proveit.Theory() # the theorem's theory
%proving _psi_t_output
# don't combine factors of 2
Mult.change_simplification_directives(combine_all_exponents=False,
combine_numeric_rational_exponents=False)
_psi_t_def
_psi_t = _psi_t_def.instantiate()
_psi_t_ket_is_normalized_vec
_psi_t_ket_is_normalized_vec.instantiate()
QPE1_def
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
phase_kickbacks_on_register
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)),
subtract(t, one), zero, order='decreasing'))
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase),
subtract(t, one), zero, order='decreasing'))
kickbacks = phase_kickbacks_on_register.instantiate(
{m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
kickbacks.inner_expr().lhs.operand)
For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:
from proveit.numbers import Complex
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
replacements=[psi_t_tensor_u__expansion.derive_reversed()])
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
equiv = output_consolidation.apply_transitivity(output_consolidation_from_desired)
equiv.sub_right_side_into(kickbacks_with_QPE1)
_psi_t_output may now be readily provable (assuming required theorems are usable). Simply execute "%qed".
%qed
proveit.physics.quantum.QPE._psi_t_output has been proven.
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | generalization | 1 | ⊢ | |
| 1 | instantiation | 4, 2, 3 | ||
| 2 | instantiation | 4, 5, 6 | ||
| 3 | instantiation | 7, 8, 9 | ||
| 4 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.rhs_prob_via_equiv | ||||
| 5 | instantiation | 10, 463, 751, 11, 12, 303, 13, 14, 15, 744, 746, 272, 16* | ||
| 6 | modus ponens | 17, 18 | ||
| 7 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.equiv_transitivity | ||||
| 8 | modus ponens | 19, 20 | ||
| 9 | instantiation | 31, 21 | ||
| 10 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.phase_kickbacks_on_register | ||||
| 11 | instantiation | 601, 22, 651, 360 | ||
| 12 | modus ponens | 23, 24 | ||
| 13 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._normalized_ket_u | ||||
| 14 | instantiation | 601, 25, 651, 360 | ||
| 15 | modus ponens | 26, 27 | ||
| 16 | instantiation | 688, 674, 736, 689, 28, 29, 690, 712, 693, 702, 703, 692 | ||
| 17 | instantiation | 47, 748, 469, 30 | ||
| 18 | instantiation | 31, 32 | ||
| 19 | instantiation | 47, 736, 748, 689, 48, 690 | ⊢ | |
| 20 | instantiation | 670, 33, 34 | ||
| 21 | modus ponens | 35, 36 | ||
| 22 | instantiation | 670, 37, 416 | ||
| 23 | instantiation | 418, 740, 741, 419 | ||
| 24 | generalization | 38 | ||
| 25 | instantiation | 670, 39, 416 | ||
| 26 | instantiation | 418, 740, 741, 419 | ||
| 27 | generalization | 40 | ||
| 28 | instantiation | 694 | ⊢ | |
| 29 | instantiation | 704 | ⊢ | |
| 30 | instantiation | 601, 41, 651, 360 | ||
| 31 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.equiv_reversal | ||||
| 32 | instantiation | 42, 463, 751, 59 | ||
| 33 | instantiation | 670, 43, 44 | ||
| 34 | instantiation | 238, 469, 67, 45, 46 | ||
| 35 | instantiation | 47, 736, 748, 689, 48, 690 | ⊢ | |
| 36 | instantiation | 82, 654, 49, 751, 463, 50, 51, 303, 52, 53, 54, 55, 56, 270, 541, 689, 469, 96, 57, 553* | ||
| 37 | instantiation | 464, 465 | ||
| 38 | instantiation | 58, 61, 358, 59 | ||
| 39 | instantiation | 464, 465 | ||
| 40 | instantiation | 60, 61, 705, 62 | ||
| 41 | instantiation | 670, 63, 416 | ||
| 42 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE.QPE1_def | ||||
| 43 | instantiation | 670, 64, 65 | ||
| 44 | instantiation | 238, 469, 66, 67, 68 | ||
| 45 | instantiation | 69, 469 | ||
| 46 | instantiation | 393, 743, 327, 328, 329, 330* | ||
| 47 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.circuit_equiv_temporal_sub | ||||
| 48 | instantiation | 704 | ⊢ | |
| 49 | instantiation | 704 | ⊢ | |
| 50 | instantiation | 704 | ⊢ | |
| 51 | instantiation | 70, 71 | ||
| 52 | instantiation | 601, 72, 73, 74 | ⊢ | |
| 53 | instantiation | 611, 75 | ⊢ | |
| 54 | instantiation | 704 | ⊢ | |
| 55 | instantiation | 611, 76 | ⊢ | |
| 56 | instantiation | 601, 77, 577, 78 | ⊢ | |
| 57 | instantiation | 181, 674, 79, 184, 80, 186 | ||
| 58 | conjecture | ⊢ | ||
| proveit.linear_algebra.matrices.exponentiation.U_closure | ||||
| 59 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._unitary_U | ||||
| 60 | conjecture | ⊢ | ||
| proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application | ||||
| 61 | instantiation | 413, 736, 81 | ||
| 62 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._eigen_uu | ||||
| 63 | instantiation | 464, 465 | ||
| 64 | instantiation | 82, 431, 83, 652, 84, 463, 85, 86, 87, 303, 88, 89, 90, 91, 92, 93, 94, 270, 169, 689, 95, 96, 97, 553, 98, 99*, 100*, 101* | ||
| 65 | instantiation | 238, 469, 102, 103, 104 | ||
| 66 | instantiation | 601, 105, 651, 360 | ||
| 67 | instantiation | 601, 106, 651, 360 | ||
| 68 | instantiation | 293, 294, 295, 441* | ||
| 69 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_from1_len_typical_eq | ||||
| 70 | theorem | ⊢ | ||
| proveit.logic.booleans.conjunction.left_from_and | ||||
| 71 | instantiation | 107, 751 | ||
| 72 | instantiation | 108 | ⊢ | |
| 73 | instantiation | 669 | ⊢ | |
| 74 | instantiation | 611, 109 | ⊢ | |
| 75 | instantiation | 214, 110, 553 | ⊢ | |
| 76 | instantiation | 268, 110, 541 | ⊢ | |
| 77 | instantiation | 111 | ⊢ | |
| 78 | instantiation | 611, 112 | ⊢ | |
| 79 | instantiation | 694 | ⊢ | |
| 80 | instantiation | 611, 443 | ||
| 81 | instantiation | 548, 113 | ||
| 82 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.output_consolidation | ||||
| 83 | instantiation | 601, 114, 130, 125 | ||
| 84 | instantiation | 357, 730, 741, 652, 289 | ||
| 85 | instantiation | 601, 115, 130, 125 | ||
| 86 | instantiation | 409, 116, 208 | ||
| 87 | modus ponens | 117, 118 | ||
| 88 | instantiation | 601, 119, 120, 121 | ||
| 89 | instantiation | 611, 122 | ||
| 90 | instantiation | 611, 123 | ||
| 91 | instantiation | 601, 124, 130, 125 | ||
| 92 | instantiation | 611, 126 | ||
| 93 | instantiation | 657, 127, 128 | ||
| 94 | instantiation | 601, 129, 130, 131 | ||
| 95 | modus ponens | 132, 133 | ||
| 96 | instantiation | 388, 469, 414 | ||
| 97 | instantiation | 134, 736, 384, 748, 135, 530, 136, 137 | ||
| 98 | instantiation | 657, 138, 139 | ||
| 99 | instantiation | 657, 140, 141 | ||
| 100 | instantiation | 657, 142, 143 | ⊢ | |
| 101 | instantiation | 657, 144, 145 | ||
| 102 | instantiation | 601, 146, 651, 360 | ||
| 103 | instantiation | 601, 147, 651, 360 | ||
| 104 | instantiation | 293, 294, 295 | ||
| 105 | instantiation | 350, 654, 148, 352, 353, 354, 384, 355* | ||
| 106 | instantiation | 670, 149, 416 | ||
| 107 | conjecture | ⊢ | ||
| proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec | ||||
| 108 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_3 | ||||
| 109 | instantiation | 670, 150, 151 | ⊢ | |
| 110 | instantiation | 388, 736, 379 | ⊢ | |
| 111 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_2 | ||||
| 112 | instantiation | 670, 152, 153 | ⊢ | |
| 113 | instantiation | 587, 735, 154 | ||
| 114 | instantiation | 350, 172, 155, 174, 175, 354, 384, 176* | ||
| 115 | instantiation | 350, 172, 156, 174, 175, 354, 384, 176* | ||
| 116 | instantiation | 409, 157, 158 | ||
| 117 | instantiation | 418, 730, 741, 289 | ||
| 118 | generalization | 159 | ||
| 119 | instantiation | 350, 172, 160, 161, 175, 354, 465, 162* | ||
| 120 | instantiation | 681, 712, 662 | ||
| 121 | instantiation | 611, 163 | ||
| 122 | instantiation | 214, 168, 553 | ||
| 123 | instantiation | 238, 469, 221, 164, 165 | ||
| 124 | instantiation | 350, 172, 166, 174, 175, 354, 384, 176* | ||
| 125 | instantiation | 611, 167 | ||
| 126 | instantiation | 268, 168, 169 | ||
| 127 | instantiation | 611, 170 | ||
| 128 | instantiation | 611, 171 | ||
| 129 | instantiation | 350, 172, 173, 174, 175, 354, 384, 176* | ||
| 130 | instantiation | 669 | ⊢ | |
| 131 | instantiation | 611, 177 | ||
| 132 | instantiation | 418, 740, 741, 419 | ||
| 133 | generalization | 178 | ||
| 134 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.disassociate | ||||
| 135 | instantiation | 704 | ⊢ | |
| 136 | instantiation | 601, 179, 484, 180 | ||
| 137 | instantiation | 181, 182, 183, 184, 515, 185, 186 | ||
| 138 | instantiation | 599, 187 | ||
| 139 | instantiation | 657, 188, 189 | ||
| 140 | instantiation | 599, 190 | ||
| 141 | instantiation | 611, 191 | ||
| 142 | instantiation | 599, 192 | ⊢ | |
| 143 | instantiation | 194, 652 | ⊢ | |
| 144 | instantiation | 599, 193 | ||
| 145 | instantiation | 194, 195 | ||
| 146 | instantiation | 350, 654, 196, 352, 353, 354, 384, 355* | ||
| 147 | instantiation | 670, 197, 416 | ||
| 148 | instantiation | 704 | ⊢ | |
| 149 | instantiation | 464, 465 | ||
| 150 | instantiation | 464, 198 | ⊢ | |
| 151 | instantiation | 657, 199, 200 | ⊢ | |
| 152 | instantiation | 464, 201 | ⊢ | |
| 153 | instantiation | 657, 202, 203 | ⊢ | |
| 154 | instantiation | 204, 740, 741, 738 | ||
| 155 | instantiation | 694 | ⊢ | |
| 156 | instantiation | 694 | ⊢ | |
| 157 | instantiation | 557, 558, 472, 205 | ||
| 158 | instantiation | 599, 206 | ||
| 159 | instantiation | 409, 207, 208 | ||
| 160 | instantiation | 694 | ⊢ | |
| 161 | instantiation | 694 | ⊢ | |
| 162 | instantiation | 657, 209, 210 | ||
| 163 | instantiation | 670, 211, 212 | ||
| 164 | instantiation | 601, 213, 651, 360 | ||
| 165 | instantiation | 214, 294, 400, 441* | ||
| 166 | instantiation | 694 | ⊢ | |
| 167 | instantiation | 468, 378 | ||
| 168 | instantiation | 444, 215, 216 | ||
| 169 | instantiation | 657, 217, 218 | ||
| 170 | instantiation | 238, 469, 222, 219, 220 | ||
| 171 | instantiation | 238, 469, 221, 222, 223 | ||
| 172 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat3 | ||||
| 173 | instantiation | 694 | ⊢ | |
| 174 | instantiation | 694 | ⊢ | |
| 175 | instantiation | 694 | ⊢ | |
| 176 | instantiation | 657, 224, 225 | ||
| 177 | instantiation | 670, 226, 227 | ||
| 178 | instantiation | 444, 228, 229 | ||
| 179 | instantiation | 670, 230, 530 | ||
| 180 | instantiation | 611, 231 | ||
| 181 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.and_if_all | ||||
| 182 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.nat4 | ||||
| 183 | instantiation | 232 | ⊢ | |
| 184 | instantiation | 669 | ⊢ | |
| 185 | modus ponens | 233, 234 | ||
| 186 | instantiation | 669 | ⊢ | |
| 187 | instantiation | 605, 748, 689, 690, 237, 646, 662 | ||
| 188 | instantiation | 643, 689, 674, 748, 690, 235, 237, 662, 646, 682 | ||
| 189 | instantiation | 614, 736, 689, 236, 690, 237, 662, 682 | ||
| 190 | instantiation | 238, 469, 239, 301, 240 | ||
| 191 | instantiation | 599, 241, 242* | ||
| 192 | instantiation | 599, 553 | ⊢ | |
| 193 | instantiation | 599, 348 | ||
| 194 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.unary_multi_output_reduction | ||||
| 195 | instantiation | 243, 244, 245 | ||
| 196 | instantiation | 704 | ⊢ | |
| 197 | instantiation | 464, 465 | ||
| 198 | instantiation | 505, 674, 246, 736, 379, 748 | ⊢ | |
| 199 | instantiation | 599, 483 | ⊢ | |
| 200 | instantiation | 637, 689, 736, 748, 690, 247, 712, 634, 682, 248* | ⊢ | |
| 201 | instantiation | 505, 674, 249, 748, 379 | ⊢ | |
| 202 | instantiation | 599, 483 | ⊢ | |
| 203 | instantiation | 637, 689, 736, 748, 690, 353, 682, 634, 250* | ⊢ | |
| 204 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.interval_upper_bound | ||||
| 205 | instantiation | 519, 558, 520, 251 | ||
| 206 | instantiation | 599, 252 | ||
| 207 | instantiation | 557, 558, 472, 253 | ||
| 208 | instantiation | 599, 254 | ⊢ | |
| 209 | instantiation | 457, 674, 255, 256, 460, 416 | ||
| 210 | instantiation | 657, 257, 258 | ||
| 211 | instantiation | 464, 259 | ||
| 212 | instantiation | 657, 260, 261 | ||
| 213 | instantiation | 350, 654, 262, 352, 353, 354, 384, 355* | ||
| 214 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.partition_front | ||||
| 215 | instantiation | 742, 263, 264 | ||
| 216 | instantiation | 496, 265 | ||
| 217 | instantiation | 643, 689, 736, 748, 690, 381, 662, 682, 646 | ||
| 218 | instantiation | 266, 682, 662, 617 | ||
| 219 | instantiation | 601, 267, 651, 360 | ||
| 220 | instantiation | 268, 269, 270, 271* | ||
| 221 | instantiation | 599, 272 | ||
| 222 | instantiation | 599, 273 | ||
| 223 | instantiation | 393, 710, 327, 274, 275, 276* | ||
| 224 | instantiation | 457, 674, 277, 278, 460, 530 | ||
| 225 | instantiation | 657, 279, 280 | ||
| 226 | instantiation | 464, 281 | ||
| 227 | instantiation | 657, 282, 283 | ||
| 228 | instantiation | 742, 735, 746 | ||
| 229 | instantiation | 620, 666, 542, 284, 285, 286*, 287* | ||
| 230 | instantiation | 464, 384 | ||
| 231 | instantiation | 468, 288 | ||
| 232 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_4_typical_eq | ||||
| 233 | instantiation | 418, 730, 741, 289 | ||
| 234 | generalization | 290 | ||
| 235 | instantiation | 694 | ⊢ | |
| 236 | instantiation | 704 | ⊢ | |
| 237 | instantiation | 749, 728, 291 | ||
| 238 | conjecture | ⊢ | ||
| proveit.core_expr_types.operations.operands_substitution_via_tuple | ||||
| 239 | instantiation | 601, 292, 651, 360 | ||
| 240 | instantiation | 293, 294, 295 | ||
| 241 | instantiation | 296, 751 | ||
| 242 | instantiation | 297, 689, 465, 748, 690, 416, 298, 299, 300, 301, 302, 303 | ||
| 243 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.pos_int_is_natural_pos | ||||
| 244 | instantiation | 742, 720, 746 | ||
| 245 | instantiation | 304, 475, 640, 305, 306, 307*, 308* | ||
| 246 | instantiation | 694 | ⊢ | |
| 247 | instantiation | 704 | ⊢ | |
| 248 | instantiation | 657, 309, 310 | ⊢ | |
| 249 | instantiation | 694 | ⊢ | |
| 250 | instantiation | 657, 311, 680 | ⊢ | |
| 251 | instantiation | 557, 558, 312, 560 | ||
| 252 | instantiation | 599, 313 | ||
| 253 | instantiation | 519, 558, 520, 314 | ||
| 254 | instantiation | 315, 712 | ⊢ | |
| 255 | instantiation | 694 | ⊢ | |
| 256 | instantiation | 694 | ⊢ | |
| 257 | instantiation | 605, 748, 689, 690, 682, 662 | ||
| 258 | instantiation | 637, 689, 736, 748, 690, 606, 682, 662, 680* | ||
| 259 | instantiation | 749, 511, 316 | ||
| 260 | instantiation | 599, 483 | ⊢ | |
| 261 | instantiation | 601, 317, 318, 319 | ||
| 262 | instantiation | 704 | ⊢ | |
| 263 | instantiation | 749, 750, 431 | ||
| 264 | instantiation | 696, 320, 433 | ⊢ | |
| 265 | instantiation | 572, 321 | ||
| 266 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_23 | ||||
| 267 | instantiation | 322, 323, 324* | ||
| 268 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.partition_back | ||||
| 269 | instantiation | 444, 325, 326 | ||
| 270 | instantiation | 581, 634, 682, 553 | ⊢ | |
| 271 | instantiation | 641, 682, 662, 617 | ||
| 272 | instantiation | 393, 743, 327, 328, 329, 330* | ||
| 273 | instantiation | 657, 331, 332 | ||
| 274 | instantiation | 611, 333 | ||
| 275 | instantiation | 611, 334 | ⊢ | |
| 276 | instantiation | 643, 689, 736, 748, 690, 335, 336, 646, 662 | ||
| 277 | instantiation | 694 | ⊢ | |
| 278 | instantiation | 694 | ⊢ | |
| 279 | instantiation | 643, 748, 736, 645, 682, 662, 646 | ||
| 280 | instantiation | 615, 689, 748, 690, 682, 662, 617 | ||
| 281 | instantiation | 505, 674, 337, 469, 379, 748 | ||
| 282 | instantiation | 599, 483 | ⊢ | |
| 283 | instantiation | 635, 748, 662, 682 | ||
| 284 | instantiation | 522, 729, 716 | ||
| 285 | instantiation | 338, 542, 729, 716, 339, 340 | ||
| 286 | instantiation | 601, 341, 342, 343 | ||
| 287 | instantiation | 601, 344, 345, 346 | ||
| 288 | instantiation | 444, 698, 347 | ||
| 289 | instantiation | 620, 542, 716, 678, 621, 438*, 471* | ||
| 290 | instantiation | 611, 348 | ||
| 291 | instantiation | 749, 731, 349 | ||
| 292 | instantiation | 350, 654, 351, 352, 353, 354, 384, 355* | ||
| 293 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.merge_front | ||||
| 294 | instantiation | 388, 689, 507 | ||
| 295 | instantiation | 611, 400 | ||
| 296 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._psi_t_def | ||||
| 297 | conjecture | ⊢ | ||
| proveit.linear_algebra.tensors.tensor_prod_disassociation | ||||
| 298 | instantiation | 601, 356, 651, 360 | ||
| 299 | instantiation | 357, 740, 741, 558, 419 | ||
| 300 | instantiation | 594, 358 | ⊢ | |
| 301 | instantiation | 601, 359, 651, 360 | ||
| 302 | modus ponens | 361, 362 | ||
| 303 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._u_ket_register | ||||
| 304 | conjecture | ⊢ | ||
| proveit.numbers.addition.strong_bound_via_left_term_bound | ||||
| 305 | instantiation | 522, 695, 721 | ||
| 306 | instantiation | 363, 640, 695, 721, 364, 365 | ||
| 307 | instantiation | 601, 366, 367, 368 | ||
| 308 | instantiation | 601, 369, 370, 371 | ||
| 309 | instantiation | 599, 372 | ⊢ | |
| 310 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.add_2_1 | ||||
| 311 | instantiation | 599, 373 | ⊢ | |
| 312 | instantiation | 711, 595, 374 | ||
| 313 | instantiation | 599, 375 | ||
| 314 | instantiation | 557, 558, 376, 560 | ||
| 315 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.complex_x_to_first_power_is_x | ||||
| 316 | instantiation | 490, 736, 689, 377, 690, 378, 379, 748, 491 | ||
| 317 | instantiation | 643, 689, 736, 690, 381, 380, 662, 682, 634 | ||
| 318 | instantiation | 635, 736, 748, 381, 662, 682 | ||
| 319 | instantiation | 637, 748, 736, 689, 606, 690, 662, 682, 680* | ||
| 320 | instantiation | 708, 382 | ⊢ | |
| 321 | instantiation | 608, 431 | ||
| 322 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.extended_range_len | ||||
| 323 | instantiation | 383, 384 | ||
| 324 | instantiation | 657, 385, 386 | ||
| 325 | instantiation | 742, 744, 495 | ||
| 326 | instantiation | 496, 387 | ||
| 327 | instantiation | 388, 389, 507 | ||
| 328 | instantiation | 611, 390 | ||
| 329 | instantiation | 611, 391 | ||
| 330 | instantiation | 657, 392, 586 | ||
| 331 | instantiation | 393, 740, 394, 395, 396 | ||
| 332 | modus ponens | 397, 398 | ||
| 333 | instantiation | 657, 399, 400 | ||
| 334 | instantiation | 657, 401, 553 | ⊢ | |
| 335 | instantiation | 704 | ⊢ | |
| 336 | instantiation | 749, 728, 402 | ||
| 337 | instantiation | 694 | ⊢ | |
| 338 | conjecture | ⊢ | ||
| proveit.numbers.ordering.less_eq_add_right | ||||
| 339 | instantiation | 421, 740, 741, 738 | ||
| 340 | instantiation | 403, 748 | ⊢ | |
| 341 | instantiation | 643, 689, 736, 748, 690, 589, 649, 682, 642 | ||
| 342 | instantiation | 643, 736, 689, 589, 645, 690, 649, 682, 662, 646 | ||
| 343 | instantiation | 657, 404, 423 | ||
| 344 | instantiation | 643, 689, 736, 748, 690, 405, 723, 682, 642 | ||
| 345 | instantiation | 643, 736, 689, 405, 645, 690, 723, 682, 662, 646 | ||
| 346 | instantiation | 615, 748, 689, 690, 723, 682, 662, 617 | ||
| 347 | instantiation | 496, 621 | ||
| 348 | instantiation | 657, 406, 407 | ||
| 349 | instantiation | 749, 734, 408 | ||
| 350 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.general_len | ||||
| 351 | instantiation | 704 | ⊢ | |
| 352 | instantiation | 704 | ⊢ | |
| 353 | instantiation | 704 | ⊢ | |
| 354 | instantiation | 409, 748, 460 | ⊢ | |
| 355 | instantiation | 657, 410, 411 | ||
| 356 | instantiation | 670, 412, 416 | ||
| 357 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.redundant_conjunction_general | ||||
| 358 | instantiation | 413, 736, 414 | ⊢ | |
| 359 | instantiation | 670, 415, 416 | ||
| 360 | instantiation | 611, 417 | ||
| 361 | instantiation | 418, 740, 741, 419 | ||
| 362 | generalization | 420 | ||
| 363 | conjecture | ⊢ | ||
| proveit.numbers.ordering.less_eq_add_right_strong | ||||
| 364 | instantiation | 421, 730, 741, 726 | ||
| 365 | instantiation | 608, 654 | ⊢ | |
| 366 | instantiation | 643, 689, 736, 748, 690, 644, 649, 712, 424 | ||
| 367 | instantiation | 643, 736, 689, 644, 633, 690, 649, 712, 662, 683 | ||
| 368 | instantiation | 657, 422, 423 | ||
| 369 | instantiation | 643, 689, 736, 748, 690, 425, 677, 712, 424 | ||
| 370 | instantiation | 643, 736, 689, 425, 633, 690, 677, 712, 662, 683 | ||
| 371 | instantiation | 615, 748, 689, 690, 677, 712, 662, 577 | ||
| 372 | instantiation | 426, 712 | ⊢ | |
| 373 | instantiation | 426, 682 | ⊢ | |
| 374 | instantiation | 670, 427, 428 | ||
| 375 | instantiation | 599, 429 | ||
| 376 | instantiation | 711, 595, 430 | ||
| 377 | instantiation | 704 | ⊢ | |
| 378 | instantiation | 749, 511, 431 | ||
| 379 | instantiation | 696, 432, 433 | ⊢ | |
| 380 | instantiation | 704 | ⊢ | |
| 381 | instantiation | 704 | ⊢ | |
| 382 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.zero_set_within_int | ||||
| 383 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_len_is_nat | ||||
| 384 | instantiation | 670, 507, 434 | ||
| 385 | instantiation | 599, 600 | ||
| 386 | instantiation | 601, 435, 436, 437 | ||
| 387 | instantiation | 620, 542, 716, 678, 621, 438*, 514* | ||
| 388 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_closure_bin | ||||
| 389 | instantiation | 749, 511, 439 | ⊢ | |
| 390 | instantiation | 657, 440, 441 | ||
| 391 | instantiation | 657, 442, 443 | ||
| 392 | instantiation | 643, 689, 736, 748, 690, 616, 619, 649, 662 | ||
| 393 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.shift_equivalence | ||||
| 394 | instantiation | 444, 445, 446 | ||
| 395 | instantiation | 611, 447 | ||
| 396 | instantiation | 611, 448 | ||
| 397 | instantiation | 449, 744, 746 | ||
| 398 | generalization | 450 | ||
| 399 | instantiation | 599, 453 | ⊢ | |
| 400 | instantiation | 657, 451, 452 | ||
| 401 | instantiation | 599, 453 | ⊢ | |
| 402 | instantiation | 749, 731, 454 | ||
| 403 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_lower_bound | ||||
| 404 | instantiation | 615, 748, 689, 690, 649, 682, 662, 617 | ||
| 405 | instantiation | 704 | ⊢ | |
| 406 | instantiation | 643, 689, 674, 748, 690, 455, 677, 646, 662, 682 | ||
| 407 | instantiation | 614, 748, 689, 690, 677, 682, 662 | ||
| 408 | instantiation | 749, 725, 456 | ||
| 409 | theorem | ⊢ | ||
| proveit.logic.equality.sub_left_side_into | ||||
| 410 | instantiation | 457, 736, 458, 459, 460, 530 | ||
| 411 | instantiation | 657, 461, 462 | ||
| 412 | instantiation | 464, 465 | ||
| 413 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_natpos_closure | ||||
| 414 | instantiation | 749, 511, 463 | ⊢ | |
| 415 | instantiation | 464, 465 | ||
| 416 | instantiation | 657, 466, 467 | ||
| 417 | instantiation | 468, 469 | ||
| 418 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.conjunction_from_quantification | ||||
| 419 | instantiation | 620, 542, 715, 678, 536, 470*, 471* | ||
| 420 | instantiation | 557, 558, 472, 473 | ||
| 421 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.interval_lower_bound | ||||
| 422 | instantiation | 615, 748, 689, 690, 649, 712, 662, 577 | ||
| 423 | instantiation | 474, 662, 651 | ||
| 424 | instantiation | 749, 728, 475 | ||
| 425 | instantiation | 704 | ⊢ | |
| 426 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_right | ||||
| 427 | instantiation | 701, 673, 476 | ||
| 428 | instantiation | 657, 477, 478 | ||
| 429 | instantiation | 599, 539 | ||
| 430 | instantiation | 670, 479, 480 | ||
| 431 | instantiation | 571, 751, 652 | ||
| 432 | instantiation | 708, 481 | ⊢ | |
| 433 | instantiation | 482, 483 | ⊢ | |
| 434 | instantiation | 601, 539, 484, 485 | ||
| 435 | instantiation | 643, 748, 736, 633, 634, 662, 683, 712 | ||
| 436 | instantiation | 635, 689, 674, 690, 486, 662, 683, 712 | ||
| 437 | instantiation | 618, 712, 662, 577 | ||
| 438 | instantiation | 601, 487, 488, 489 | ||
| 439 | instantiation | 490, 748, 689, 690, 491 | ⊢ | |
| 440 | instantiation | 599, 632 | ||
| 441 | instantiation | 657, 492, 493 | ||
| 442 | instantiation | 599, 632 | ||
| 443 | instantiation | 590, 662 | ||
| 444 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nonneg_int_is_natural | ||||
| 445 | instantiation | 742, 494, 495 | ||
| 446 | instantiation | 496, 497 | ||
| 447 | instantiation | 657, 498, 499 | ||
| 448 | instantiation | 581, 662, 500, 682, 514 | ||
| 449 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_fn_transformation | ||||
| 450 | instantiation | 657, 501, 502 | ||
| 451 | instantiation | 643, 689, 736, 748, 690, 589, 649, 682 | ||
| 452 | instantiation | 637, 748, 736, 689, 606, 690, 649, 682, 680* | ||
| 453 | instantiation | 661, 682 | ⊢ | |
| 454 | instantiation | 749, 734, 503 | ||
| 455 | instantiation | 694 | ⊢ | |
| 456 | assumption | |||
| 457 | axiom | ⊢ | ||
| proveit.core_expr_types.operations.operands_substitution | ||||
| 458 | instantiation | 704 | ⊢ | |
| 459 | instantiation | 704 | ⊢ | |
| 460 | instantiation | 641, 682, 617 | ⊢ | |
| 461 | instantiation | 643, 748, 736, 689, 645, 690, 682, 662, 646 | ||
| 462 | instantiation | 504, 682, 662, 617 | ||
| 463 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._s_in_nat_pos | ||||
| 464 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_len | ||||
| 465 | instantiation | 505, 674, 506, 689, 507, 748 | ||
| 466 | instantiation | 599, 539 | ||
| 467 | instantiation | 601, 508, 509, 510 | ||
| 468 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_from1_len | ||||
| 469 | instantiation | 749, 511, 751 | ||
| 470 | instantiation | 657, 512, 513 | ||
| 471 | instantiation | 601, 514, 617, 515 | ||
| 472 | instantiation | 516, 682, 517, 518 | ⊢ | |
| 473 | instantiation | 519, 558, 520, 521 | ||
| 474 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_reverse | ||||
| 475 | instantiation | 522, 678, 523 | ||
| 476 | instantiation | 670, 524, 525 | ||
| 477 | instantiation | 688, 748, 674, 689, 526, 690, 673, 702, 597, 692 | ||
| 478 | instantiation | 688, 689, 736, 674, 690, 675, 526, 712, 693, 702, 597, 692 | ||
| 479 | instantiation | 701, 673, 527 | ||
| 480 | instantiation | 657, 528, 529 | ||
| 481 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.zero_set_within_nat | ||||
| 482 | conjecture | ⊢ | ||
| proveit.logic.sets.enumeration.fold_singleton | ||||
| 483 | conjecture | ⊢ | ||
| proveit.numbers.negation.negated_zero | ||||
| 484 | instantiation | 669 | ⊢ | |
| 485 | instantiation | 611, 530 | ||
| 486 | instantiation | 694 | ⊢ | |
| 487 | instantiation | 657, 531, 532 | ||
| 488 | instantiation | 581, 607, 662, 712, 533 | ||
| 489 | instantiation | 669 | ⊢ | |
| 490 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_pos_from_nonneg | ||||
| 491 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.less_0_1 | ||||
| 492 | instantiation | 643, 689, 736, 748, 690, 589, 649, 682, 662 | ||
| 493 | instantiation | 534, 662, 682, 651 | ||
| 494 | instantiation | 749, 750, 535 | ⊢ | |
| 495 | instantiation | 745, 730 | ||
| 496 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.nonneg_difference | ||||
| 497 | instantiation | 620, 640, 715, 678, 536, 537*, 538* | ||
| 498 | instantiation | 599, 539 | ||
| 499 | instantiation | 657, 540, 541 | ||
| 500 | instantiation | 749, 728, 542 | ||
| 501 | instantiation | 599, 543 | ||
| 502 | instantiation | 657, 544, 545 | ||
| 503 | instantiation | 749, 546, 547 | ||
| 504 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_13 | ||||
| 505 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_closure | ||||
| 506 | instantiation | 694 | ⊢ | |
| 507 | instantiation | 548, 549 | ||
| 508 | instantiation | 643, 748, 736, 645, 634, 662, 646, 682 | ||
| 509 | instantiation | 635, 689, 674, 690, 550, 662, 646, 682 | ||
| 510 | instantiation | 618, 682, 662, 617 | ||
| 511 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat | ||||
| 512 | instantiation | 643, 748, 736, 689, 589, 690, 634, 649, 682 | ||
| 513 | instantiation | 635, 689, 736, 690, 589, 649, 682 | ||
| 514 | instantiation | 657, 551, 552 | ||
| 515 | instantiation | 611, 553 | ⊢ | |
| 516 | conjecture | ⊢ | ||
| proveit.numbers.division.div_complex_closure | ||||
| 517 | instantiation | 554, 712 | ⊢ | |
| 518 | instantiation | 555, 593, 556 | ⊢ | |
| 519 | conjecture | ⊢ | ||
| proveit.linear_algebra.addition.binary_closure | ||||
| 520 | conjecture | ⊢ | ||
| proveit.physics.quantum.algebra.ket_zero_in_qubit_space | ||||
| 521 | instantiation | 557, 558, 559, 560 | ||
| 522 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_real_closure_bin | ||||
| 523 | instantiation | 561, 721 | ⊢ | |
| 524 | instantiation | 701, 562, 692 | ||
| 525 | instantiation | 688, 689, 736, 748, 690, 563, 702, 597, 692 | ||
| 526 | instantiation | 694 | ⊢ | |
| 527 | instantiation | 670, 564, 565 | ||
| 528 | instantiation | 688, 748, 674, 689, 676, 690, 673, 702, 630, 692 | ||
| 529 | instantiation | 688, 689, 736, 674, 690, 675, 676, 712, 693, 702, 630, 692 | ||
| 530 | instantiation | 657, 566, 567 | ||
| 531 | instantiation | 643, 748, 736, 689, 589, 690, 682, 649 | ||
| 532 | instantiation | 657, 568, 569 | ||
| 533 | instantiation | 670, 576, 570 | ||
| 534 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_31 | ||||
| 535 | instantiation | 571, 652 | ⊢ | |
| 536 | instantiation | 572, 573 | ||
| 537 | instantiation | 657, 574, 575 | ||
| 538 | instantiation | 601, 576, 577, 578 | ||
| 539 | instantiation | 631, 649, 682, 632* | ||
| 540 | instantiation | 657, 579, 580 | ||
| 541 | instantiation | 581, 682, 712, 680 | ⊢ | |
| 542 | instantiation | 749, 731, 582 | ||
| 543 | instantiation | 643, 748, 736, 689, 589, 690, 619, 649, 682 | ||
| 544 | instantiation | 643, 689, 674, 736, 690, 583, 584, 619, 649, 682, 646, 662 | ||
| 545 | instantiation | 657, 585, 586 | ||
| 546 | instantiation | 739, 730, 744 | ||
| 547 | assumption | |||
| 548 | conjecture | ⊢ | ||
| proveit.numbers.negation.nat_closure | ||||
| 549 | instantiation | 587, 740, 588 | ||
| 550 | instantiation | 694 | ⊢ | |
| 551 | instantiation | 643, 748, 736, 689, 589, 690, 662, 649, 682 | ||
| 552 | instantiation | 641, 662, 682, 651 | ||
| 553 | instantiation | 590, 682 | ⊢ | |
| 554 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.sqrt_complex_closure | ||||
| 555 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_rational_non_zero__not_zero | ||||
| 556 | instantiation | 591, 592, 593 | ⊢ | |
| 557 | conjecture | ⊢ | ||
| proveit.linear_algebra.scalar_multiplication.scalar_mult_closure | ||||
| 558 | instantiation | 594, 654 | ⊢ | |
| 559 | instantiation | 711, 595, 596 | ||
| 560 | conjecture | ⊢ | ||
| proveit.physics.quantum.algebra.ket_one_in_qubit_space | ||||
| 561 | conjecture | ⊢ | ||
| proveit.numbers.negation.real_closure | ||||
| 562 | instantiation | 701, 702, 597 | ||
| 563 | instantiation | 704 | ⊢ | |
| 564 | instantiation | 701, 598, 692 | ||
| 565 | instantiation | 688, 689, 736, 748, 690, 691, 702, 630, 692 | ||
| 566 | instantiation | 599, 600 | ||
| 567 | instantiation | 601, 602, 603, 604 | ||
| 568 | instantiation | 605, 748, 689, 690, 682, 649 | ||
| 569 | instantiation | 637, 689, 736, 748, 690, 606, 682, 649, 680* | ||
| 570 | instantiation | 681, 662, 607 | ||
| 571 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_pos_closure_bin | ||||
| 572 | conjecture | ⊢ | ||
| proveit.numbers.ordering.relax_less | ||||
| 573 | instantiation | 608, 751 | ||
| 574 | instantiation | 643, 748, 736, 689, 644, 690, 634, 649, 712 | ||
| 575 | instantiation | 635, 689, 736, 690, 644, 649, 712 | ||
| 576 | instantiation | 657, 609, 610 | ||
| 577 | instantiation | 669 | ⊢ | |
| 578 | instantiation | 611, 680 | ⊢ | |
| 579 | instantiation | 657, 612, 613 | ||
| 580 | instantiation | 614, 689, 748, 690, 662, 712, 646 | ||
| 581 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.subtract_from_add | ||||
| 582 | instantiation | 749, 734, 740 | ||
| 583 | instantiation | 694 | ⊢ | |
| 584 | instantiation | 704 | ⊢ | |
| 585 | instantiation | 615, 736, 689, 748, 616, 690, 619, 649, 682, 662, 617 | ||
| 586 | instantiation | 618, 662, 619, 651 | ||
| 587 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos | ||||
| 588 | instantiation | 620, 668, 716, 678, 621, 622*, 623* | ||
| 589 | instantiation | 704 | ⊢ | |
| 590 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_left | ||||
| 591 | conjecture | ⊢ | ||
| proveit.numbers.division.div_rational_nonzero_closure | ||||
| 592 | instantiation | 749, 625, 624 | ⊢ | |
| 593 | instantiation | 749, 625, 626 | ⊢ | |
| 594 | conjecture | ⊢ | ||
| proveit.linear_algebra.complex_vec_set_is_vec_space | ||||
| 595 | instantiation | 749, 728, 627 | ⊢ | |
| 596 | instantiation | 670, 628, 629 | ||
| 597 | instantiation | 711, 712, 642 | ||
| 598 | instantiation | 701, 702, 630 | ||
| 599 | axiom | ⊢ | ||
| proveit.logic.equality.substitution | ||||
| 600 | instantiation | 631, 649, 712, 632* | ||
| 601 | conjecture | ⊢ | ||
| proveit.logic.equality.four_chain_transitivity | ||||
| 602 | instantiation | 643, 748, 736, 633, 634, 662, 683, 682 | ||
| 603 | instantiation | 635, 689, 674, 690, 636, 662, 683, 682 | ||
| 604 | instantiation | 637, 748, 736, 689, 638, 690, 662, 683, 682, 639* | ||
| 605 | conjecture | ⊢ | ||
| proveit.numbers.addition.leftward_commutation | ||||
| 606 | instantiation | 704 | ⊢ | |
| 607 | instantiation | 749, 728, 640 | ||
| 608 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos | ||||
| 609 | instantiation | 643, 748, 736, 689, 644, 690, 662, 649, 712 | ||
| 610 | instantiation | 641, 662, 712, 651 | ||
| 611 | theorem | ⊢ | ||
| proveit.logic.equality.equals_reversal | ||||
| 612 | instantiation | 643, 689, 736, 748, 690, 644, 649, 712, 642 | ||
| 613 | instantiation | 643, 736, 689, 644, 645, 690, 649, 712, 662, 646 | ||
| 614 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_general_rev | ||||
| 615 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_general | ||||
| 616 | instantiation | 704 | ⊢ | |
| 617 | instantiation | 669 | ⊢ | |
| 618 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_32 | ||||
| 619 | instantiation | 749, 728, 647 | ||
| 620 | conjecture | ⊢ | ||
| proveit.numbers.addition.weak_bound_via_left_term_bound | ||||
| 621 | instantiation | 648, 751 | ||
| 622 | instantiation | 681, 682, 649 | ||
| 623 | instantiation | 650, 662, 651 | ||
| 624 | instantiation | 749, 653, 652 | ⊢ | |
| 625 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero | ||||
| 626 | instantiation | 749, 653, 654 | ⊢ | |
| 627 | instantiation | 749, 718, 655 | ⊢ | |
| 628 | instantiation | 701, 673, 656 | ||
| 629 | instantiation | 657, 658, 659 | ||
| 630 | instantiation | 711, 712, 660 | ||
| 631 | conjecture | ⊢ | ||
| proveit.numbers.negation.distribute_neg_through_binary_sum | ||||
| 632 | instantiation | 661, 662 | ||
| 633 | instantiation | 704 | ⊢ | |
| 634 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.zero_is_complex | ||||
| 635 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_any | ||||
| 636 | instantiation | 694 | ⊢ | |
| 637 | conjecture | ⊢ | ||
| proveit.numbers.addition.association | ||||
| 638 | instantiation | 704 | ⊢ | |
| 639 | instantiation | 670, 663, 664 | ⊢ | |
| 640 | instantiation | 749, 731, 665 | ||
| 641 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_12 | ||||
| 642 | instantiation | 749, 728, 666 | ||
| 643 | conjecture | ⊢ | ||
| proveit.numbers.addition.disassociation | ||||
| 644 | instantiation | 704 | ⊢ | |
| 645 | instantiation | 704 | ⊢ | |
| 646 | instantiation | 722, 682 | ⊢ | |
| 647 | instantiation | 749, 731, 667 | ||
| 648 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound | ||||
| 649 | instantiation | 749, 728, 668 | ||
| 650 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_basic | ||||
| 651 | instantiation | 669 | ⊢ | |
| 652 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat1 | ||||
| 653 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int | ||||
| 654 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat2 | ||||
| 655 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.e_is_real_pos | ||||
| 656 | instantiation | 670, 671, 672 | ||
| 657 | axiom | ⊢ | ||
| proveit.logic.equality.equals_transitivity | ||||
| 658 | instantiation | 688, 748, 674, 689, 676, 690, 673, 702, 703, 692 | ||
| 659 | instantiation | 688, 689, 736, 674, 690, 675, 676, 712, 693, 702, 703, 692 | ||
| 660 | instantiation | 722, 677 | ||
| 661 | conjecture | ⊢ | ||
| proveit.numbers.negation.double_negation | ||||
| 662 | instantiation | 749, 728, 678 | ||
| 663 | instantiation | 679, 682, 712, 680 | ⊢ | |
| 664 | instantiation | 681, 682, 683 | ⊢ | |
| 665 | instantiation | 749, 734, 730 | ||
| 666 | instantiation | 749, 731, 684 | ||
| 667 | instantiation | 749, 734, 685 | ||
| 668 | instantiation | 749, 731, 686 | ||
| 669 | axiom | ⊢ | ||
| proveit.logic.equality.equals_reflexivity | ||||
| 670 | theorem | ⊢ | ||
| proveit.logic.equality.sub_right_side_into | ||||
| 671 | instantiation | 701, 687, 692 | ||
| 672 | instantiation | 688, 689, 736, 748, 690, 691, 702, 703, 692 | ||
| 673 | instantiation | 701, 712, 693 | ⊢ | |
| 674 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.nat3 | ||||
| 675 | instantiation | 704 | ⊢ | |
| 676 | instantiation | 694 | ⊢ | |
| 677 | instantiation | 749, 728, 695 | ||
| 678 | instantiation | 696, 697, 751 | ||
| 679 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.subtract_from_add_reversed | ||||
| 680 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.add_1_1 | ||||
| 681 | conjecture | ⊢ | ||
| proveit.numbers.addition.commutation | ||||
| 682 | instantiation | 749, 728, 716 | ⊢ | |
| 683 | instantiation | 722, 712 | ⊢ | |
| 684 | instantiation | 749, 734, 698 | ||
| 685 | instantiation | 749, 699, 700 | ||
| 686 | instantiation | 749, 734, 743 | ||
| 687 | instantiation | 701, 702, 703 | ||
| 688 | conjecture | ⊢ | ||
| proveit.numbers.multiplication.disassociation | ||||
| 689 | axiom | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
| 690 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq | ||||
| 691 | instantiation | 704 | ⊢ | |
| 692 | instantiation | 749, 728, 705 | ⊢ | |
| 693 | instantiation | 749, 728, 706 | ⊢ | |
| 694 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq | ||||
| 695 | instantiation | 749, 731, 707 | ||
| 696 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.unfold_subset_eq | ||||
| 697 | instantiation | 708, 709 | ⊢ | |
| 698 | instantiation | 742, 746, 710 | ||
| 699 | instantiation | 739, 744, 746 | ||
| 700 | assumption | |||
| 701 | conjecture | ⊢ | ||
| proveit.numbers.multiplication.mult_complex_closure_bin | ||||
| 702 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.i_is_complex | ||||
| 703 | instantiation | 711, 712, 713 | ||
| 704 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq | ||||
| 705 | instantiation | 714, 715, 716, 717 | ⊢ | |
| 706 | instantiation | 749, 718, 719 | ⊢ | |
| 707 | instantiation | 749, 734, 720 | ||
| 708 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.relax_proper_subset | ||||
| 709 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.nat_pos_within_real | ||||
| 710 | instantiation | 745, 744 | ⊢ | |
| 711 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_complex_closure | ||||
| 712 | instantiation | 749, 728, 721 | ⊢ | |
| 713 | instantiation | 722, 723 | ||
| 714 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real | ||||
| 715 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.zero_is_real | ||||
| 716 | instantiation | 749, 731, 724 | ⊢ | |
| 717 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._phase_in_interval | ||||
| 718 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.real_pos_within_real | ||||
| 719 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.pi_is_real_pos | ||||
| 720 | instantiation | 749, 725, 726 | ||
| 721 | instantiation | 749, 731, 727 | ⊢ | |
| 722 | conjecture | ⊢ | ||
| proveit.numbers.negation.complex_closure | ||||
| 723 | instantiation | 749, 728, 729 | ||
| 724 | instantiation | 749, 734, 744 | ⊢ | |
| 725 | instantiation | 739, 730, 741 | ||
| 726 | assumption | |||
| 727 | instantiation | 749, 734, 733 | ⊢ | |
| 728 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.real_within_complex | ||||
| 729 | instantiation | 749, 731, 732 | ||
| 730 | instantiation | 742, 743, 733 | ||
| 731 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.rational_within_real | ||||
| 732 | instantiation | 749, 734, 735 | ||
| 733 | instantiation | 749, 747, 736 | ⊢ | |
| 734 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.rational_numbers.int_within_rational | ||||
| 735 | instantiation | 749, 737, 738 | ||
| 736 | theorem | ⊢ | ||
| proveit.numbers.numerals.decimals.nat2 | ||||
| 737 | instantiation | 739, 740, 741 | ||
| 738 | assumption | |||
| 739 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.int_interval_within_int | ||||
| 740 | instantiation | 742, 743, 744 | ||
| 741 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.zero_is_int | ||||
| 742 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_int_closure_bin | ||||
| 743 | instantiation | 745, 746 | ||
| 744 | instantiation | 749, 747, 748 | ⊢ | |
| 745 | conjecture | ⊢ | ||
| proveit.numbers.negation.int_closure | ||||
| 746 | instantiation | 749, 750, 751 | ||
| 747 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_within_int | ||||
| 748 | theorem | ⊢ | ||
| proveit.numbers.numerals.decimals.nat1 | ||||
| 749 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
| 750 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_pos_within_int | ||||
| 751 | assumption | |||
| *equality replacement requirements | ||||